nominal2: Nominal/Ex/CoreHaskell.thy@66114fa3d2ee (annotated)

2083 9568f9f31822 tuned file names for examples Christian Urban <urbanc@in.tum.de> parents: 2064 diff changeset	1	theory CoreHaskell
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	2	imports "../Nominal2"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2142 diff changeset	5	(* Core Haskell *)
2100 705dc7532ee3 added comment about bind_set Christian Urban <urbanc@in.tum.de> parents: 2095 diff changeset	6
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	atom_decl var
1698 69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	8	atom_decl cvar
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	atom_decl tvar
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	11	nominal_datatype core_haskell:
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	12	tkind =
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	KStar
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	\| KFun "tkind" "tkind"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	and ckind =
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	CKEq "ty" "ty"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	and ty =
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	TVar "tvar"
1684 b9e4c812d2c6 Core Haskell can now use proper strings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1667 diff changeset	19	\| TC "string"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	\| TApp "ty" "ty"
1684 b9e4c812d2c6 Core Haskell can now use proper strings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1667 diff changeset	21	\| TFun "string" "ty_lst"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2630 diff changeset	22	\| TAll tv::"tvar" "tkind" T::"ty" binds (set) tv in T
1698 69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	23	\| TEq "ckind" "ty"
1606 75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	24	and ty_lst =
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	25	TsNil
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	26	\| TsCons "ty" "ty_lst"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	and co =
1699 2dca07aca287 small changes in the core-haskell spec Christian Urban <urbanc@in.tum.de> parents: 1698 diff changeset	28	CVar "cvar"
1698 69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	29	\| CConst "string"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	\| CApp "co" "co"
1684 b9e4c812d2c6 Core Haskell can now use proper strings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1667 diff changeset	31	\| CFun "string" "co_lst"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2630 diff changeset	32	\| CAll cv::"cvar" "ckind" C::"co" binds (set) cv in C
1698 69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	33	\| CEq "ckind" "co"
69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	34	\| CRefl "ty"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	\| CSym "co"
1698 69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	36	\| CCir "co" "co"
69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	37	\| CAt "co" "ty"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38	\| CLeft "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	\| CRight "co"
1698 69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	40	\| CSim "co" "co"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	\| CRightc "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	\| CLeftc "co"
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	\| CCoe "co" "co"
1606 75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	44	and co_lst =
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	45	CsNil
75403378068b Initial list unfoldings in Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1601 diff changeset	46	\| CsCons "co" "co_lst"
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	47	and trm =
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	48	Var "var"
1699 2dca07aca287 small changes in the core-haskell spec Christian Urban <urbanc@in.tum.de> parents: 1698 diff changeset	49	\| K "string"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2630 diff changeset	50	\| LAMT tv::"tvar" "tkind" t::"trm" binds (set) tv in t
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2630 diff changeset	51	\| LAMC cv::"cvar" "ckind" t::"trm" binds (set) cv in t
1698 69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	52	\| AppT "trm" "ty"
69472e74bd3b Update according to paper Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1695 diff changeset	53	\| AppC "trm" "co"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2630 diff changeset	54	\| Lam v::"var" "ty" t::"trm" binds (set) v in t
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55	\| App "trm" "trm"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2630 diff changeset	56	\| Let x::"var" "ty" "trm" t::"trm" binds (set) x in t
1609 c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	57	\| Case "trm" "assoc_lst"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	58	\| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	59	and assoc_lst =
c9bc3b61046c Modification to Core Haskell to make it accepted with an empty binding function. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1606 diff changeset	60	ANil
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2630 diff changeset	61	\| ACons p::"pat" t::"trm" "assoc_lst" binds "bv p" in t
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	62	and pat =
1700 b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	63	Kpat "string" "tvars" "cvars" "vars"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	64	and vars =
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	65	VsNil
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	66	\| VsCons "var" "ty" "vars"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	67	and tvars =
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	68	TvsNil
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	69	\| TvsCons "tvar" "tkind" "tvars"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	70	and cvars =
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	71	CvsNil
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	72	\| CvsCons "cvar" "ckind" "cvars"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	73	binder
1695 e42ee5947b5c Changed to Lists. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1688 diff changeset	74	bv :: "pat \<Rightarrow> atom list"
1700 b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	75	and bv_vs :: "vars \<Rightarrow> atom list"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	76	and bv_tvs :: "tvars \<Rightarrow> atom list"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	77	and bv_cvs :: "cvars \<Rightarrow> atom list"
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	78	where
1700 b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	79	"bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	80	\| "bv_vs VsNil = []"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	81	\| "bv_vs (VsCons v k t) = (atom v) # bv_vs t"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	82	\| "bv_tvs TvsNil = []"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	83	\| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
b5141d1ab24f Initial renaming Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1699 diff changeset	84	\| "bv_cvs CvsNil = []"
2213 231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2142 diff changeset	85	\| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2142 diff changeset	86
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	87	(* generated theorems *)
2406 428d9cb9a243 can also lift the various eqvt lemmas for bn, fv, fv_bn and size Christian Urban <urbanc@in.tum.de> parents: 2405 diff changeset	88
2598 b136721eedb2 automated permute_bn theorems Christian Urban <urbanc@in.tum.de> parents: 2593 diff changeset	89	thm core_haskell.permute_bn
2593 25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	90	thm core_haskell.perm_bn_alpha
25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	91	thm core_haskell.perm_bn_simps
25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	92	thm core_haskell.bn_finite
25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	93
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	94	thm core_haskell.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	95	thm core_haskell.induct
2630 8268b277d240 automated all strong induction lemmas Christian Urban <urbanc@in.tum.de> parents: 2629 diff changeset	96	thm core_haskell.inducts
8268b277d240 automated all strong induction lemmas Christian Urban <urbanc@in.tum.de> parents: 2629 diff changeset	97	thm core_haskell.strong_induct
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	98	thm core_haskell.exhaust
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	99	thm core_haskell.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	100	thm core_haskell.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	101	thm core_haskell.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	102	thm core_haskell.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	103	thm core_haskell.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	104	thm core_haskell.size_eqvt
2481 3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	105	thm core_haskell.supp
2339 1e0b3992189c more quotient-definitions Christian Urban <urbanc@in.tum.de> parents: 2336 diff changeset	106
1868 26c0c35641cb equivariance for alpha_raw in CoreHaskell is automatically derived Christian Urban <urbanc@in.tum.de> parents: 1867 diff changeset	107
1601 5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	108	end
5f0bb35114c3 Added missing file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	109

author	Christian Urban <urbanc@in.tum.de>
	Thu, 19 Apr 2018 13:58:22 +0100 (2018-04-19)
branch	Nominal2-Isabelle2016-1
changeset 3246	66114fa3d2ee
parent 2950	0911cb7bf696
permissions	-rw-r--r--