<commit_before>(*  Title:      HOL/Univ
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

For univ.thy
*)

open Univ;

(** apfst -- can be used in similar type definitions **)

goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)";
by (rtac split 1);
qed "apfst_conv";

val [major,minor] = goal Univ.thy
    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R \
\    |] ==> R";
by (rtac PairE 1);
by (rtac minor 1);
by (assume_tac 1);
by (rtac (major RS trans) 1);
by (etac ssubst 1);
by (rtac apfst_conv 1);
qed "apfst_convE";

(** Push -- an injection, analogous to Cons on lists **)

val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> i=j";
by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
by (rtac nat_case_0 1);
by (rtac nat_case_0 1);
qed "Push_inject1";

val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> f=g";
by (rtac (major RS fun_cong RS ext RS box_equals) 1);
by (rtac (nat_case_Suc RS ext) 1);
by (rtac (nat_case_Suc RS ext) 1);
qed "Push_inject2";

val [major,minor] = goal Univ.thy
    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P \
\    |] ==> P";
by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
qed "Push_inject";

val [major] = goalw Univ.thy [Push_def] "Push k f =(%z.0) ==> P";
by (rtac (major RS fun_cong RS box_equals RS Suc_neq_Zero) 1);
by (rtac nat_case_0 1);
by (rtac refl 1);
qed "Push_neq_K0";

(*** Isomorphisms ***)

goal Univ.thy "inj(Rep_Node)";
by (rtac inj_inverseI 1);       (*cannot combine by RS: multiple unifiers*)
by (rtac Rep_Node_inverse 1);
qed "inj_Rep_Node";

goal Univ.thy "inj_onto Abs_Node Node";
by (rtac inj_onto_inverseI 1);
by (etac Abs_Node_inverse 1);
qed "inj_onto_Abs_Node";

val Abs_Node_inject = inj_onto_Abs_Node RS inj_ontoD;


(*** Introduction rules for Node ***)

goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
by (Blast_tac 1);
qed "Node_K0_I";

goalw Univ.thy [Node_def,Push_def]
    "!!p. p: Node ==> apfst (Push i) p : Node";
by (blast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
qed "Node_Push_I";


(*** Distinctness of constructors ***)

(** Scons vs Atom **)

goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M$N) ~= Atom(a)";
by (rtac notI 1);
by (etac (equalityD2 RS subsetD RS UnE) 1);
by (rtac singletonI 1);
by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, 
                          Pair_inject, sym RS Push_neq_K0] 1
     ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
qed "Scons_not_Atom";
bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym);


(*** Injectiveness ***)

(** Atomic nodes **)

goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
by (blast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
qed "inj_Atom";
val Atom_inject = inj_Atom RS injD;

goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
by (blast_tac (!claset addSDs [Atom_inject]) 1);
qed "Atom_Atom_eq";
AddIffs [Atom_Atom_eq];

goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
by (rtac injI 1);
by (etac (Atom_inject RS Inl_inject) 1);
qed "inj_Leaf";

val Leaf_inject = inj_Leaf RS injD;
AddSDs [Leaf_inject];

goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
by (rtac injI 1);
by (etac (Atom_inject RS Inr_inject) 1);
qed "inj_Numb";

val Numb_inject = inj_Numb RS injD;
AddSDs [Numb_inject];

(** Injectiveness of Push_Node **)

val [major,minor] = goalw Univ.thy [Push_Node_def]
    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P \
\    |] ==> P";
by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1));
by (etac (sym RS apfst_convE) 1);
by (rtac minor 1);
by (etac Pair_inject 1);
by (etac (Push_inject1 RS sym) 1);
by (rtac (inj_Rep_Node RS injD) 1);
by (etac trans 1);
by (safe_tac (!claset addSEs [Push_inject,sym]));
qed "Push_Node_inject";


(** Injectiveness of Scons **)

goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma1";

goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";

val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
qed "Scons_inject1";

val [major] = goal Univ.thy "M$N = M'$N' ==> N=N'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
qed "Scons_inject2";

val [major,minor] = goal Univ.thy
    "[| M$N = M'$N';  [| M=M';  N=N' |] ==> P \
\    |] ==> P";
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
qed "Scons_inject";

AddSDs [Scons_inject];

goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
by (blast_tac (!claset addSEs [Scons_inject]) 1);
qed "Scons_Scons_eq";

(*** Distinctness involving Leaf and Numb ***)

(** Scons vs Leaf **)

goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
by (rtac Scons_not_Atom 1);
qed "Scons_not_Leaf";
bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);
<commit_msg>Removed "AddSDs [Scons_inject];" because (a) IT WAS WRONG (should have been AddSEs) (b) It was redundant (due to the AddIffs [...,Scons_Scons_eq])<commit_after>(*  Title:      HOL/Univ
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

For univ.thy
*)

open Univ;

(** apfst -- can be used in similar type definitions **)

goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)";
by (rtac split 1);
qed "apfst_conv";

val [major,minor] = goal Univ.thy
    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R \
\    |] ==> R";
by (rtac PairE 1);
by (rtac minor 1);
by (assume_tac 1);
by (rtac (major RS trans) 1);
by (etac ssubst 1);
by (rtac apfst_conv 1);
qed "apfst_convE";

(** Push -- an injection, analogous to Cons on lists **)

val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> i=j";
by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
by (rtac nat_case_0 1);
by (rtac nat_case_0 1);
qed "Push_inject1";

val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> f=g";
by (rtac (major RS fun_cong RS ext RS box_equals) 1);
by (rtac (nat_case_Suc RS ext) 1);
by (rtac (nat_case_Suc RS ext) 1);
qed "Push_inject2";

val [major,minor] = goal Univ.thy
    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P \
\    |] ==> P";
by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
qed "Push_inject";

val [major] = goalw Univ.thy [Push_def] "Push k f =(%z.0) ==> P";
by (rtac (major RS fun_cong RS box_equals RS Suc_neq_Zero) 1);
by (rtac nat_case_0 1);
by (rtac refl 1);
qed "Push_neq_K0";

(*** Isomorphisms ***)

goal Univ.thy "inj(Rep_Node)";
by (rtac inj_inverseI 1);       (*cannot combine by RS: multiple unifiers*)
by (rtac Rep_Node_inverse 1);
qed "inj_Rep_Node";

goal Univ.thy "inj_onto Abs_Node Node";
by (rtac inj_onto_inverseI 1);
by (etac Abs_Node_inverse 1);
qed "inj_onto_Abs_Node";

val Abs_Node_inject = inj_onto_Abs_Node RS inj_ontoD;


(*** Introduction rules for Node ***)

goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
by (Blast_tac 1);
qed "Node_K0_I";

goalw Univ.thy [Node_def,Push_def]
    "!!p. p: Node ==> apfst (Push i) p : Node";
by (blast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
qed "Node_Push_I";


(*** Distinctness of constructors ***)

(** Scons vs Atom **)

goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M$N) ~= Atom(a)";
by (rtac notI 1);
by (etac (equalityD2 RS subsetD RS UnE) 1);
by (rtac singletonI 1);
by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, 
                          Pair_inject, sym RS Push_neq_K0] 1
     ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
qed "Scons_not_Atom";
bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym);


(*** Injectiveness ***)

(** Atomic nodes **)

goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
by (blast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
qed "inj_Atom";
val Atom_inject = inj_Atom RS injD;

goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
by (blast_tac (!claset addSDs [Atom_inject]) 1);
qed "Atom_Atom_eq";
AddIffs [Atom_Atom_eq];

goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
by (rtac injI 1);
by (etac (Atom_inject RS Inl_inject) 1);
qed "inj_Leaf";

val Leaf_inject = inj_Leaf RS injD;
AddSDs [Leaf_inject];

goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
by (rtac injI 1);
by (etac (Atom_inject RS Inr_inject) 1);
qed "inj_Numb";

val Numb_inject = inj_Numb RS injD;
AddSDs [Numb_inject];

(** Injectiveness of Push_Node **)

val [major,minor] = goalw Univ.thy [Push_Node_def]
    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P \
\    |] ==> P";
by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1));
by (etac (sym RS apfst_convE) 1);
by (rtac minor 1);
by (etac Pair_inject 1);
by (etac (Push_inject1 RS sym) 1);
by (rtac (inj_Rep_Node RS injD) 1);
by (etac trans 1);
by (safe_tac (!claset addSEs [Push_inject,sym]));
qed "Push_Node_inject";


(** Injectiveness of Scons **)

goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma1";

goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";

val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
qed "Scons_inject1";

val [major] = goal Univ.thy "M$N = M'$N' ==> N=N'";
by (rtac (major RS equalityE) 1);
by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
qed "Scons_inject2";

val [major,minor] = goal Univ.thy
    "[| M$N = M'$N';  [| M=M';  N=N' |] ==> P \
\    |] ==> P";
by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
qed "Scons_inject";

goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
by (blast_tac (!claset addSEs [Scons_inject]) 1);
qed "Scons_Scons_eq";

(*** Distinctness involving Leaf and Numb ***)

(** Scons vs Leaf **)

goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
by (rtac Scons_not_Atom 1);
qed "Scons_not_Leaf";
bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);

{'fraction_non_alphanumeric': 0.1705216297299913, 'fraction_numerical': 0.0152908158327688, 'mean_word_length': 4.436086270384008, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 37, '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': '4177380', 'n_tokens_mistral': 4885, 'n_tokens_neox': 4527, 'n_words': 1300}