<commit_before>(** Inductive definitions how-to *)

(**
   Required theorems
*)

let outl_thm = thm "outl_thm"
let outr_thm = thm "outr_thm"

let isl_thm1 = 
  prove << !x: (isl (inl x)) = true >>
  (cut (thm "isl_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let isl_thm2 = 
  prove << !x: (isl (inr x)) = false >>
  (cut (thm "isl_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let isr_thm1 = 
  prove << !x: (isr (inr x)) = true >>
  (cut (thm "isr_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let isr_thm2 = 
  prove << !x: (isr (inl x)) = false >>
  (cut (thm "isr_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let implies_l1=
  prove << !x: (true => x) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let implies_l2=
  prove << !x: (false => x) = true >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l1 = 
prove << !x: (true & x) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l2 = 
prove << !x: (false & x) = false >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l3 = 
prove << !x: (x & true) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l4 = 
prove << !x: (x & x) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

(** Start of example theory *)

let _ = begin_theory "indefeg" [];;


(** Single induction *)

let empty = declare << empty: 'a >>;; 
let add= declare << add : 'a -> 'b -> 'b >>;;
let in_def = declare << in: 'a -> 'b -> bool >>;;

(**
   finite empty;
   [ ~x in A; finite A ] --> finite (add x A);
*)

let finite_def=
  define 
  <:def<
    finite X =
  !P:
    ((P empty)
     & (! x A: (~(x in A) & (P A)) => (P (add x A))))
  => (P X)
  >>;;

let finite_induct =
  prove 
  <<
  !P:
    ((P empty)
     & (! x A: (~(x in A) & (P A)) => (P (add x A))))
  => 
  !A : (finite A) => (P A)
  >>
  (flatten_tac 
   ++ unfold "finite"
   ++ back_tac
   ++ blast_tac ++ back_tac ++ blast_tac);;  


let finite_rules = 
  prove 
  << 
    (finite empty)
  & (!x A: (~(x in A) & (finite A)) => (finite (add x A)))
  >>
    (rewrite_tac [defn "finite"]
     ++ blast_tac
     ++ (match_asm << !P: A => (P x) >>
	 (fun l -> instA ~a:l [ << _P >> ]))
     ++ (implA -- [split_tac ++ basic])
     ++ back_tac 
     ++ blast_tac);;

let finite_cases =
  prove 
  <<
    !X:
    (finite X) =
  ((X = empty) | (? x A: (~(x in A) & (finite A)) & (X = (add x A))))
  >>
    (specC ++ equals_tac ++ iffC 
     --
     [
       (* => *)
       cut ~inst:
	 [<< %X: 
	     (X = empty)
	 | (?x A: (~(in x A) & (finite A)) & X = (add x A))
	   >>]
	 finite_induct
       ++ betaA
       ++ implA -- [match_concl << (finite A) => B >> deleteC; 
		    instA [<<_X>>] ++ basic]
       ++ conjC
       --
	 [
	   (* 1 *)
	   (repeat disjC) ++ eq_tac;
	   (* 2 *)
	   flatten_tac ++ disjA
	   --
	     [
	       (* 1 *)
	       instC [ << _x >>; <<_A>>]
	       ++ simp_tac [finite_rules]
	       ++ blast_tac;
	       (* 2 *)
	       flatten_tac
	       ++ (match_concl << ? X: Y >> liftC)
	       ++ instC [<< _x >> ; << add _x1 _A1 >>]
	       ++ simp_tac [finite_rules]
	     ]
	 ];
       (* <= *)
       cut finite_rules
	 ++ scatter_tac
	 ++ simp
	 ++ back_tac
	 ++ simp
     ]);;

(** Mutual induction *)

let zero = declare << zero: 'a >>;; 
let succ= declare << succ : 'a -> 'a >>;;

(**
   even zero;
   [ even x ] --> odd (succ x);<commit_msg>Minor tweaks<commit_after>(** Inductive definitions how-to *)

(**
   Required theorems
*)

let outl_thm = thm "outl_thm"
let outr_thm = thm "outr_thm"

let isl_thm1 = 
  prove << !x: (isl (inl x)) = true >>
  (cut (thm "isl_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let isl_thm2 = 
  prove << !x: (isl (inr x)) = false >>
  (cut (thm "isl_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let isr_thm1 = 
  prove << !x: (isr (inr x)) = true >>
  (cut (thm "isr_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let isr_thm2 = 
  prove << !x: (isr (inl x)) = false >>
  (cut (thm "isr_thm") 
   ++ conjA
   ++ rewriteC_tac [thm "true_prop"; thm "false_prop"]
   ++ basic);;

let implies_l1=
  prove << !x: (true => x) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let implies_l2=
  prove << !x: (false => x) = true >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l1 = 
prove << !x: (true & x) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l2 = 
prove << !x: (false & x) = false >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l3 = 
prove << !x: (x & true) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

let conj_l4 = 
prove << !x: (x & x) = x >>
  (flatten_tac ++ equals_tac ++ blast_tac);;

(** Start of example theory *)

let _ = begin_theory "indefeg" [];;


(** Single induction *)

let empty = declare << empty: 'a >>;; 
let add= declare << add : 'a -> 'b -> 'b >>;;
let in_def = declare << in: 'a -> 'b -> bool >>;;

(**
   finite empty;
   [ ~x in A; finite A ] --> finite (add x A);
*)

let finite_def=
  define 
  <:def<
    finite X =
  !P:
    ((P empty)
     & (! x A: (~(x in A) & (P A)) => (P (add x A))))
  => (P X)
  >>;;

let finite_induct =
  prove 
  <<
  !P:
    ((P empty)
     & (! x A: (~(x in A) & (P A)) => (P (add x A))))
  => 
  !A : (finite A) => (P A)
  >>
  (flatten_tac 
   ++ unfold "finite"
   ++ back_tac
   ++ blast_tac ++ back_tac ++ blast_tac);;  


let finite_rules = 
  prove 
  << 
    (finite empty)
  & (!x A: (~(x in A) & (finite A)) => (finite (add x A)))
  >>
    (rewrite_tac [defn "finite"]
     ++ blast_tac
     ++ (match_asm << !P: A => (P x) >>
	 (fun l -> instA ~a:l [ << _P >> ]))
     ++ (implA -- [split_tac ++ basic])
     ++ back_tac 
     ++ blast_tac);;

let finite_cases =
  prove 
  <<
    !X:
    (finite X) =
  ((X = empty) | (? x A: (~(x in A) & (finite A)) & (X = (add x A))))
  >>
    (specC ++ equals_tac ++ iffC 
     --
     [
       (* => *)
       cut ~inst:
	 [<< %X: 
	     (X = empty)
	 | (?x A: (~(in x A) & (finite A)) & X = (add x A))
	   >>]
	 finite_induct
       ++ betaA
       ++ implA -- [match_concl << (finite A) => B >> deleteC; 
		    instA [<<_X>>] ++ basic]
       ++ conjC
       --
	 [
	   (* 1 *)
	   (repeat disjC) ++ eq_tac;
	   (* 2 *)
	   flatten_tac ++ disjA
	   --
	     [
	       (* 1 *)
	       instC [ << _x >>; <<_A>>]
	       ++ simp_tac [finite_rules]
	       ++ blast_tac;
	       (* 2 *)
	       flatten_tac
	       ++ negA ++ negA
	       ++ (match_concl << ? X: Y >> liftC)
	       ++ instC [<< _x >> ; << add _x1 _A1 >>]
	       ++ simp_tac [finite_rules]
	     ]
	 ];
       (* <= *)
       cut finite_rules
	 ++ scatter_tac
	 ++ simp
	 ++ back_tac
	 ++ simp
     ]);;

(** Mutual induction *)

let zero = declare << zero: 'a >>;; 
let succ= declare << succ : 'a -> 'a >>;;

(**
   even zero;
   [ even x ] --> odd (succ x);
{'fraction_non_alphanumeric': 0.21403057579654236, 'fraction_numerical': 0.004572081725960852, 'mean_word_length': 2.2080659945004584, 'pattern_counts': {'":': 0, '<': 121, '<?xml version=': 0, '>': 157, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3672967', 'n_tokens_mistral': 3089, 'n_tokens_neox': 2919, 'n_words': 750}